Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
f
(
g
(X),Y)
→
f
(X,
n__f
(
g
(X),
activate
(Y)))
2:
f
(X1,X2)
→
n__f
(X1,X2)
3:
activate
(
n__f
(X1,X2))
→
f
(X1,X2)
4:
activate
(X)
→ X
There are 3 dependency pairs:
5:
F
(
g
(X),Y)
→
F
(X,
n__f
(
g
(X),
activate
(Y)))
6:
F
(
g
(X),Y)
→
ACTIVATE
(Y)
7:
ACTIVATE
(
n__f
(X1,X2))
→
F
(X1,X2)
Consider the SCC {5-7}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.03 seconds) --- May 3, 2006